T:Type, Q:((T List)Prop).
Q(nil)  (ys:T List, y:T. Q(ys)  Q(ys @ [y]))  {zs:T List. Q(zs)} 

latex

Definitions	t  T, x:A. B(x), x(s), P  Q, Dec(P), ||as||, ij, P  Q, False, A, AB, , {T}, Prop, as @ bs, null(as), b, last(L), t  ...$L, P  Q, P & Q, P  Q, x:A. B(x)
Lemmas	last lemma, length append, length nil, length cons, last wf, ge wf, nat properties, append wf, nat wf, le wf, non neg length, length wf1, decidable assert, null wf